-- -*-Haskell-*-

{-
 * Copyright (c) 2007 Gabor Greif
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
 * of the Software, and to permit persons to whom the Software is furnished to do
 * so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be
 * included in all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
 * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
 * HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
 * WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE
 * OR OTHER DEALINGS IN THE SOFTWARE.
 -}

import "LangPrelude.prg"

import "Thrist.omg" 
  (Thrist, Nil, Cons, syntax List(l))

plus:: Nat ~> Nat ~> Nat
{plus Z m} = m
{plus (S n) m} = S {plus n m}

{-
canGround :: Nat' n -> Divsbl 0t n
canGround n = Ground

theorem canGround
-}

prop Divsbl :: Nat ~> Nat ~> * where
  Ground :: Divsbl 0t b
  -- Ground :: Nat' b -> Divsbl 0t (S b)
  Leap :: Divsbl a b -> Divsbl {plus a b} b
 deriving Nat(d)

data Layout :: Nat ~> Nat ~> * where
  Int :: Divsbl n 4t => Layout n (4+n)t
  Bool :: Layout n (S n)
  Pad :: Nat' p -> Layout n {plus n p}

t1 :: Thrist Layout 0t 8t
--t1 = [Pad 4v, Int]l

